Nuprl Lemma : interface-link_wf 0,22
A, B:(IdMsgA), l:IdLnk, tg:Id. interface-link(A;B;l;tg)  Prop 
latex

Definitionsinterface-link(A;B;l;tg), source(l), P & Q, Prop, destination(l), A, rcv(l,tg) declared in M, x:A. B(x), IdLnk, Id, t  T, MsgA
Lemmasmsga wf, Id wf, IdLnk wf, ma-declm wf, not wf, ldst wf, lsrc wf

origin